WARNING:  Note that MEMBER-DELETE contains the free variable U which
will be chosen by instantiating the hypothesis
(MEMBER X (DELETE U V)).


WARNING:  Note that SUBBAGP-DELETE contains the free variable U which
will be chosen by instantiating the hypothesis
(SUBBAGP X (DELETE U Y)).


WARNING:  When the linear lemma MEMBER-IMPLIES-PLUS-TREE-GREATEREQP
is stored under (MEANING (PLUS-TREE Y) A) it contains the free
variable X which will be chosen by instantiating the hypothesis
(MEMBER X Y).


WARNING:  When the linear lemma MEMBER-IMPLIES-PLUS-TREE-GREATEREQP
is stored under (MEANING X A) it contains the free variable Y which
will be chosen by instantiating the hypothesis (MEMBER X Y).


WARNING:  When the linear lemma SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP
is stored under (MEANING (PLUS-TREE Y) A) it contains the free
variable X which will be chosen by instantiating the hypothesis
(SUBBAGP X Y).


WARNING:  When the linear lemma SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP
is stored under (MEANING (PLUS-TREE X) A) it contains the free
variable Y which will be chosen by instantiating the hypothesis
(SUBBAGP X Y).


WARNING:  Note that NUMBERP-MEANING-BRIDGE contains the free variable
X which will be chosen by instantiating the hypothesis:
      (EQUAL (MEANING Z A)
	     (MEANING (PLUS-TREE X) A))
.


WARNING:  Note that MEMBER-IMPLIES-NUMBERP contains the free variable
C which will be chosen by instantiating the hypothesis:
      (MEMBER C (PLUS-FRINGE X))
.


WARNING:  Note that the rewrite rule EVEN1-DOUBLE will be stored so
as to apply only to terms with the nonrecursive function symbol EVEN1.


WARNING:  Note that CROCK-DUE-TO-LACK-OF-BOUNCE contains the free
variable L which will be chosen by instantiating the hypothesis
(EQUAL X (SORT L)).


WARNING:  Note that TAUTOLOGY-CHECKER-SOUNDNESS-BRIDGE contains the
free variables A1 and Y which will be chosen by instantiating the
hypothesis (TAUTOLOGYP Y A1).


WARNING:  Note that PRIME-BASIC contains the free variable Z which
will be chosen by instantiating the hypothesis (NOT (EQUAL Z 1.)).


WARNING:  Note that REMAINDER-GCD contains the free variable X which
will be chosen by instantiating the hypothesis (EQUAL (GCD B X) Y).


WARNING:  Note that DIVIDES-TIMES1 contains the free variable Y which
will be chosen by instantiating the hypothesis (EQUAL A (TIMES Z Y)).


WARNING:  Note that KLUDGE-BRIDGE contains the free variable K which
will be chosen by instantiating the hypothesis (EQUAL Y (TIMES K X)).


WARNING:  Note that GCD-DISTRIBUTES-OVER-AN-OPENED-UP-TIMES contains
the free variable X which will be chosen by instantiating the
hypothesis (NUMBERP X).


WARNING:  Note that PRIME-MEMBER contains the free variable L1 which
will be chosen by instantiating the hypothesis:
      (EQUAL (TIMES C (TIMES-LIST L1))
	     (TIMES-LIST L2))
.


WARNING:  META lemmas must be proved in a constructive history.  The
current history contains the nonconstructive axiom NUMBERP-CALL.  If
this metalemma is proved using unsound axioms you may get wiped out
by the application of the metafunction.


WARNING:  META lemmas must be proved in a constructive history.  The
current history contains the nonconstructive axiom NUMBERP-CALL.  If
this metalemma is proved using unsound axioms you may get wiped out
by the application of the metafunction.